<html><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"></head><body><hr><!------------------------------------------------------------------------>
<h2>E/EP 1.4pre</h2>
Stephan Schulz<br>
Technische Universit&auml;t M&uuml;nchen, Germany<br>

<h3>Architecture</h3>

E 1.4pre [<A HREF="#References">Sch2002,Sch2004</A>] is described in
this section. E is a purely equational theorem prover for full
first-order logic with equality. It consists of an (optional)
clausifier for pre-processing full first-order formulae into clausal
from, and a saturation algorithm implementing an instance of the
superposition calculus with negative literal selection and a number of
redundancy elimination techniques.  E is based on the DISCOUNT-loop
variant of the <EM>given-clause</EM> algorithm, i.e., a strict
separation of active and passive facts. No special rules for
non-equational literals have been implemented. Resolution is
effectively simulated by paramodulation and equality resolution.
<P>
EP&nbsp;1.4pre is just a combination of E&nbsp;1.4pre in verbose mode
and a proof analysis tool extracting the used inference steps. For the
LTB division, a control program uses a SInE-like analysis to extract
reduced axiomatizations that are handed to several instances of E.
</p>

<h3>Strategies</h3>

Proof search in E is primarily controlled by a literal selection
strategy, a clause evaluation heuristic, and a simplification
ordering. The prover supports a large number of pre-programmed literal
selection strategies. Clause evaluation heuristics can be constructed
on the fly by combining various parametrized primitive evaluation
functions, or can be selected from a set of predefined
heuristics. Clause evaluation heuristics are based on symbol-counting,
but also take other clause properties into account. In particular, the
search can prefer clauses from the set of support, or containing many
symbols also present in the goal. Supported term orderings are several
parametrized instances of Knuth-Bendix-Ordering (KBO) and
Lexicographic Path Ordering (LPO).
<P>
The automatic mode is based on a static partition of the set of all
clausal problems based on a number of simple features (number of
clauses, maximal symbol arity, presence of equality, presence of
non-unit and non-Horn clauses,...). Each class of clauses is
automatically assigned a heuristic that performs well on problems from
this class in test runs. About 100 different strategies have been
evaluated on all untyped first-order problems from TPTP 4.1.0.


<h3>Implementation</h3>

E is build around perfectly shared terms, i.e. each distinct term is
only represented once in a term bank. The whole set of terms thus
consists of a number of interconnected directed acyclic graphs. Term
memory is managed by a simple mark-and-sweep garbage collector.

Unconditional (forward) rewriting using unit clauses is implemented
using perfect discrimination trees with size and age
constraints. Whenever a possible simplification is detected, it is
added as a rewrite link in the term bank. As a result, not only terms,
but also rewrite steps are shared.

Subsumption and contextual literal cutting (also known as subsumption
resolution) is supported using feature vector indexing
[<A HREF="#References">Sch2004b</A>].

Superposition and backward rewriting use fingerprint indexing, a new
technique combining ideas from feature vector indexing and path
indexing.

Finally, LPO and KBO are implemented using the elegant and efficient
algorithms developed by Bernd Löchner in [<A HREF="#References">Loe2006,
Loe06b</A>].

The prover and additional information are available at the following
address:
<pre>    <a href="http://www.eprover.org/">http://www.eprover.org</a></pre>

<h3>Expected Competition Performance</h3>

E 1.4pre is relatively little changed from last years entry. The
system is expected to perform well in most proof classes, but will at
best complement top systems in the disproof classes.


<a NAME="References">
<h3>References</h3>
<dl>
<dt> Sch2002
<dd> Schulz S. (2002),
     <strong>E: A Brainiac Theorem Prover</strong>,
     <em>Journal of AI Communications</em> 15(2/3), 111-126, IOS Press
</dd>
<dt> Sch2004
<dd> Schulz S. (2004),
     <strong>System Abstract: E 0.81</strong>,
     <em>Proceedings of the 3rd IJCAR (Cork, Ireland)</em>,     
     Lecture Notes in Artificial Intelligence,
     Springer-Verlag
</dd>
<dt> Sch2004b
<dd> Schulz S. (2004),
     <strong>Simple and Efficient Clause Subsumption with Feature
     Vector Indexing</strong>,
     <em>Proceedings of the IJCAR-2004 Workshop on Empirically
     Successful First-Order Theorem Proving, (Cork, Ireland)</em>
</dd>
<dt> Loe2006
<dd> L&ouml;chner B. (2004),
     <strong>Things to know when implementing LPO</strong>,
     <em>International Journal on Artificial Intelligence Tools</em>, 
         15(1), pp.53–80, 2006.
</dd>
<DT> Loe2006b
<DD> L&ouml;chner B. (2006),
     <strong>Things to Know When Implementing KBO</strong>,
     <em>Journal of Automated Reasoning</em> 36(4),
     pp.289-310.
</dd>
</dl>
<p>

</p><hr><!------------------------------------------------------------------------>
</body></html>
